import java.io.BufferedReader;
import java.io.FileInputStream;
import java.io.InputStreamReader;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.LinkedList;

public class Parser {
	private Graph graph;
	private Hashtable<Integer, LinkedList<LinkedList<Integer>>> table = new Hashtable<Integer, LinkedList<LinkedList<Integer>>>();
	private LinkedList<int[]> clauseList = new LinkedList<int[]>();
	private int clauses = 0;
	
	public void parse(String filename, Graph g){
		graph = g;

		try{
			FileInputStream in = new FileInputStream("data.txt");
			BufferedReader br = new BufferedReader(new InputStreamReader(in));
			String strLine;
			//Read File Line By Line
			while ((strLine = br.readLine()) != null){
				if(strLine.startsWith("c") || strLine.startsWith("p")){
					continue;
				}
				
				clauses++;
				
				String[] array = strLine.split(" ");
				
				int[] clauseArray = new int[3];
				clauseArray[0] = Integer.parseInt(array[0]);
				clauseArray[1] = Integer.parseInt(array[1]);          
				clauseArray[2] = Integer.parseInt(array[2]);
				
				clauseList.add(clauseArray);
				            
				for(int i = 0; i < 3; i++){
					//System.out.println(i);
					
					if(!graph.existsNode(Integer.parseInt(array[i]))){
						graph.addNode(Integer.parseInt(array[i]));
					}
					
					if(graph.existsNode((-1*Integer.parseInt(array[i]))) && (!graph.existsEdge(Integer.parseInt(array[i]), -1*Integer.parseInt(array[i])) && !graph.existsEdge(-1*Integer.parseInt(array[i]), Integer.parseInt(array[i])))){
						graph.addEdge(Integer.parseInt(array[i]), (-1*Integer.parseInt(array[i])));
					}
					
					graph.incrWeight(Integer.parseInt(array[i]));
					
					for(int j = 0; j < 3; j++){
						//System.out.println("\t"+j);
						if(!graph.existsNode(Integer.parseInt(array[j]))){
							graph.addNode(Integer.parseInt(array[j]));
						}
						
						if(i != j && !graph.existsEdge(Integer.parseInt(array[i]), Integer.parseInt(array[j]))){
							graph.addEdge(Integer.parseInt(array[i]), Integer.parseInt(array[j]));
						}
					}
				}
			}
			in.close();
		}catch (Exception e){
			System.err.println("Error: " + e.getMessage());
		}
	}
	
	public void constructTable(){
		for(int vertex : graph.connectionsFrom.keySet()){
			LinkedList<Integer> vOfV = new LinkedList<Integer>();
			LinkedList<Integer> nsOfV = new LinkedList<Integer>();
			vOfV.add(vertex);
			for(int otherVertex : graph.connectionsFrom.get(vertex)){
				nsOfV.add(otherVertex);
			}
			LinkedList<LinkedList<Integer>> both = new LinkedList<LinkedList<Integer>>();
			both.add(vOfV);
			both.add(nsOfV);
			//System.out.println(vOfV + " " + nsOfV);
			table.put(vertex, both);
		}
	}
	
	public void removeAndAdd(Integer row){
		table.remove(row);
		
		for(int index : table.keySet()){
			if(!table.get(index).get(1).contains(row)){
				table.get(index).get(1).add(row);
			}
		}
		
		if(table.containsKey(row*-1)){
			for(int index : table.keySet()){
				// add V(~v) to all remaining VS
				for(int element : table.get(row*-1).get(0)){
					if(!table.get(index).get(0).contains(element)){
						table.get(index).get(0).add(element);
					}
				}
				// add NS(~v) to all remaining NS
				for(int element : table.get(row*-1).get(1)){
					if(!table.get(index).get(1).contains(element)){
						table.get(index).get(1).add(element);
					}
				}
			}
		}
	}
	
	public boolean containsLiteralAndInverse(LinkedList<Integer> list){
		for(int i : list){
			for(int j : list){
				if(i == -j){
					return true;
				}
			}
		}
		return false;
	}
	
	public boolean RR1(Integer row) {
		if(graph.sumOfWeights(table.get(row).get(0)) > clauses){
			removeAndAdd(row);
			return true;
		}
		return false;
	}
	
	public boolean RR2(Integer row) {
		if(graph.sumOfWeights(table.get(row).get(1)) > 2*clauses){
			removeAndAdd(row);
			return true;
		}
		return false;
	}
	
	public boolean RR3(Integer row) {
		if(containsLiteralAndInverse(table.get(row).get(0)) || containsLiteralAndInverse(table.get(row).get(0))){
			removeAndAdd(row);
			return true;
		}
		return false;
	}
	
	public boolean RR4(Integer row) {
		for(int[] array : clauseList){
			int count = 0;
			for(int i = 0; i < 3; i++){
				if(table.get(row).get(0).contains(array[i])){
					count++;
				}
			}
			if(count > 1){
				removeAndAdd(row);
				return true;
			}
		}
		return false;
	}
	
	public boolean RR5(Integer row) {
		for(int[] array : clauseList){
			int count = 0;
			for(int i = 0; i < 3; i++){
				if(table.get(row).get(1).contains(array[i])){
					count++;
				}
			}
			if(count > 2){
				removeAndAdd(row);
				return true;
			}
		}
		return false;
	}
	
	public boolean RR6(Integer row) {
		boolean flag = false;
		for(int element : table.get(row).get(0)){
			for(int element2 : table.get(row).get(1)){
				if(element == element2){
					flag = true;
				}
			}
		}
		
		if(flag){
			removeAndAdd(row);
			return true;
		}
		return false;
	}
	
	public boolean RR7(Integer row) {
		boolean hasChanged = false;
		for(int[] array : clauseList){
			int count = 0;
			int nonMatchingItem = -1;
			for(int i = 0; i < 3; i++){
				if(table.get(row).get(1).contains(array[i])){
					count++;
				}
				else
				{
					nonMatchingItem = array[i];
				}
			}
			if(count == 2){
				/*
				for(int element : table.get(nonMatchingItem).get(0)){
					if(!table.get(row).get(0).contains(element)){
						table.get(row).get(0).add(element);
						hasChanged = true;
					}
				}
				for(int element : table.get(nonMatchingItem).get(1)){
					if(!table.get(row).get(1).contains(element)){
						table.get(row).get(1).add(element);
						hasChanged = true;
					}
				}
				*/
				hasChanged = mergeRows(nonMatchingItem, row);
				return hasChanged;
			}
		}
		return false;
	}
	
	public boolean RR8(Integer row) {
		boolean hasChanged = false;
		for (Integer neighbor : table.get(row).get(1))
		{
			if (graph.existsNode(-1 * neighbor))
			{
				hasChanged |= mergeRows(-1 * neighbor, row);
			}
		}
		return hasChanged;
	}
	
	//Add V(fromRow) to V(intoRow) and NS(fromRow) to NS(intoRow).
	public boolean mergeRows(int fromRow, int intoRow)
	{
		if (table.get(intoRow).get(0).containsAll(table.get(fromRow).get(0))
			&& table.get(intoRow).get(1).containsAll(table.get(fromRow).get(1)))
		{
			return false;
		}
		LinkedList<Integer> newVertexSet = new LinkedList<Integer>();
		newVertexSet = union(table.get(intoRow).get(0), table.get(fromRow).get(0));
		LinkedList<Integer> newNeighborSet = new LinkedList< Integer >();
		newNeighborSet = union(table.get(intoRow).get(1), table.get(fromRow).get(1));
		LinkedList<LinkedList<Integer>> both = new LinkedList< LinkedList<Integer> >();
		both.add(newVertexSet);
		both.add(newNeighborSet);
		table.put(intoRow, both);
		return true;
	}
	
	public LinkedList<Integer> union(LinkedList<Integer> a, LinkedList<Integer> b)
	{
		HashSet<Integer> set = new HashSet<Integer>();
		set.addAll(a);
		set.addAll(b);
		LinkedList<Integer> result = new LinkedList<Integer>(set);		
		return result;
	}
	
	public boolean RR9(Integer row) {
		boolean applies = false;
		for (Integer otherRow : table.keySet())
		{
			boolean match = true;
			for (Integer otherNeighbor : table.get(otherRow).get(1))
			{
				if (!table.get(row).get(1).contains(otherNeighbor))
				{
					match = false;
				}
			}
			if (match)
			{
				applies = true;
				for (Integer otherVertexSetItem : table.get(otherRow).get(0))
				{
					if (!table.get(row).get(0).contains(otherVertexSetItem))
					{
						table.get(row).get(0).add(otherVertexSetItem);
					}
				}
			}
		}
		return applies;
	}
	
	public boolean solved(){
		if (table.size() == 0)
		{
			System.out.print("No solution");
			return true;
		}
		else
		{
			for (Integer row : table.keySet())
			{
				if (graph.sumOfWeights(table.get(row).get(0)) == clauses)
				{
					System.out.println("Solution found!");
					System.out.println(table.get(row).get(0));
					return true;
				}
			}
		}
		return false;
	}
	
	public void applyRules() { 
		for(Integer row : table.keySet()){
			for(int i = 1; i < 10; i++){
				if(solved()){
					System.exit(0);
				}
				switch(i){
					case 1:
						if(RR1(row)){
							i = 0;
							break;
						}
					case 2:
						if(RR2(row)){
							i = 0;
							break;
						}
					case 3:
						if(RR3(row)){
							i = 0;
							break;
						}
					case 4:
						if(RR4(row)){
							i = 0;
							break;
						}
					case 5:
						if(RR5(row)){
							i = 0;
							break;
						}
					case 6:
						if(RR6(row)){
							i = 0;
							break;
						}
					case 7:
						if(RR7(row)){
							i = 0;
							break;
						}
					case 8:
						if(RR8(row)){
							i = 0;
							break;
						}
					case 9:
						if(RR9(row)){
							i = 0;
							break;
						}
				}
			}
		}
	}
	
}
